(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 61)) (_ BitVec 64))
(declare-fun p0 ( (_ BitVec 88) (_ BitVec 36) (_ BitVec 97)) Bool)
(declare-fun v0 () (_ BitVec 109))
(assert (let ((e1(_ bv29926413727245 47)))
(let ((e2(_ bv92485418705 38)))
(let ((e3 (f0 ((_ zero_extend 14) e1))))
(let ((e4 (bvmul e3 ((_ zero_extend 17) e1))))
(let ((e5 (bvadd e3 ((_ zero_extend 17) e1))))
(let ((e6 (bvsdiv e3 e4)))
(let ((e7 (ite (p0 ((_ zero_extend 24) e3) ((_ extract 36 1) e2) ((_ extract 107 11) v0)) (_ bv1 1) (_ bv0 1))))
(let ((e8 (p0 ((_ sign_extend 24) e3) ((_ extract 35 0) e2) ((_ extract 104 8) v0))))
(let ((e9 (bvuge ((_ sign_extend 17) e1) e6)))
(let ((e10 (distinct v0 ((_ sign_extend 45) e4))))
(let ((e11 (bvugt ((_ sign_extend 71) e2) v0)))
(let ((e12 (bvult v0 ((_ zero_extend 45) e4))))
(let ((e13 (bvsge ((_ sign_extend 26) e2) e3)))
(let ((e14 (distinct e1 ((_ zero_extend 9) e2))))
(let ((e15 (bvule ((_ zero_extend 9) e2) e1)))
(let ((e16 (bvsle e3 e4)))
(let ((e17 (bvugt e3 ((_ sign_extend 17) e1))))
(let ((e18 (distinct e4 e6)))
(let ((e19 (distinct ((_ zero_extend 26) e2) e4)))
(let ((e20 (bvsle e5 ((_ sign_extend 17) e1))))
(let ((e21 (bvuge ((_ sign_extend 62) e1) v0)))
(let ((e22 (distinct ((_ zero_extend 46) e7) e1)))
(let ((e23 (and e22 e16)))
(let ((e24 (ite e14 e20 e12)))
(let ((e25 (xor e9 e18)))
(let ((e26 (and e21 e8)))
(let ((e27 (xor e25 e19)))
(let ((e28 (ite e11 e27 e24)))
(let ((e29 (= e28 e13)))
(let ((e30 (= e10 e15)))
(let ((e31 (xor e17 e29)))
(let ((e32 (xor e31 e30)))
(let ((e33 (xor e26 e26)))
(let ((e34 (= e32 e32)))
(let ((e35 (xor e34 e23)))
(let ((e36 (not e35)))
(let ((e37 (xor e36 e33)))
(let ((e38 (and e37 (not (= e4 (_ bv0 64))))))
(let ((e39 (and e38 (not (= e4 (bvnot (_ bv0 64)))))))
e39
))))))))))))))))))))))))))))))))))))))))

(check-sat)
